COM: quot_1_summary
COM: quot_1_intro
STM: quotient wf
STM: quotient qinc
STM: type inj wf for quot
STM: quot elim
STM: all quot elim
STM: dec iff ex bvfun
STM: decidable quotient equal
COM: quot_1_end
